Trait isotope::term::dynamic::DynamicValue [−][src]
pub trait DynamicValue: Debug + Any + DynHash {}Show methods
fn dyn_cons(&self, ctx: &mut dyn ConsCtx) -> Option<TermId>; fn dyn_ty(&self) -> Option<AnnotationRef<'_>>; fn dyn_ix(&self) -> Option<NodeIx>; fn dyn_code(&self) -> Code; fn dyn_is_local_ty(&self) -> Option<bool>; fn dyn_is_local_universe(&self) -> Option<bool>; fn dyn_is_root(&self) -> bool; fn dyn_is_subtype_in(
&self,
other: &Term,
ctx: &mut dyn TermEqCtxMut
) -> Option<bool>; fn dyn_universe(&self) -> Option<Universe>; fn dyn_untyped_code(&self) -> Code; fn dyn_filter(&self) -> VarFilter; fn dyn_shift(
&self,
n: i32,
base: u32,
ctx: &mut dyn ConsCtx
) -> Result<Option<TermId>, Error>; fn dyn_has_var_dep(&self, ix: u32, equiv: bool) -> bool; fn dyn_has_dep_below(&self, ix: u32, base: u32) -> bool; fn dyn_load_flags(&self) -> TyckFlags; fn dyn_set_flags(&self, flags: TyckFlags); fn dyn_eq_in(
&self,
other: &dyn DynamicValue,
ctx: &mut dyn TermEqCtxMut
) -> Option<bool>; fn as_any(&self) -> &dyn Any; fn dyn_eq_term_in(
&self,
other: &Term,
ctx: &mut dyn TermEqCtxMut
) -> Option<bool> { ... } fn dyn_eq_id_in(
&self,
other: &TermId,
ctx: &mut dyn TermEqCtxMut
) -> Option<bool> { ... }
Expand description
The interface which must be implemented by dynamic terms
Rather than implement this manually, it is usually preferable to implement
Value
, which will implement this trait automatically assuming the type
also satisfies Debug
, Hash
, PartialEq
, and 'static
.
Required methods
Cons this term within a given context. Return None
if already consed.
fn dyn_ty(&self) -> Option<AnnotationRef<'_>>
[src]
fn dyn_ty(&self) -> Option<AnnotationRef<'_>>
[src]Get the type annotation of this term
Get the index of this term in an isotope
program graph, if any
fn dyn_is_local_ty(&self) -> Option<bool>
[src]
fn dyn_is_local_ty(&self) -> Option<bool>
[src]Get whether this term is a type
fn dyn_is_local_universe(&self) -> Option<bool>
[src]
fn dyn_is_local_universe(&self) -> Option<bool>
[src]Get whether this term is a universe
fn dyn_is_root(&self) -> bool
[src]
fn dyn_is_root(&self) -> bool
[src]Get whether this term is in “root form”
fn dyn_is_subtype_in(
&self,
other: &Term,
ctx: &mut dyn TermEqCtxMut
) -> Option<bool>
[src]
fn dyn_is_subtype_in(
&self,
other: &Term,
ctx: &mut dyn TermEqCtxMut
) -> Option<bool>
[src]Get whether this term is a subtype of another term in a given context
fn dyn_universe(&self) -> Option<Universe>
[src]
fn dyn_universe(&self) -> Option<Universe>
[src]Get whether this term has a universe in all contexts
fn dyn_untyped_code(&self) -> Code
[src]
fn dyn_untyped_code(&self) -> Code
[src]Get the untyped hash-code of this term
fn dyn_filter(&self) -> VarFilter
[src]
fn dyn_filter(&self) -> VarFilter
[src]Get the variable filter of this term
Shift this term’s variables with index >= base
up by n
in a given context
fn dyn_has_var_dep(&self, ix: u32, equiv: bool) -> bool
[src]
fn dyn_has_var_dep(&self, ix: u32, equiv: bool) -> bool
[src]Whether this term has a given variable dependency
fn dyn_has_dep_below(&self, ix: u32, base: u32) -> bool
[src]
fn dyn_has_dep_below(&self, ix: u32, base: u32) -> bool
[src]Whether this term has a given variable dependency below ix
and above base
fn dyn_load_flags(&self) -> TyckFlags
[src]
fn dyn_load_flags(&self) -> TyckFlags
[src]Load this term’s flags
fn dyn_set_flags(&self, flags: TyckFlags)
[src]
fn dyn_set_flags(&self, flags: TyckFlags)
[src]Set this term’s flags
fn dyn_eq_in(
&self,
other: &dyn DynamicValue,
ctx: &mut dyn TermEqCtxMut
) -> Option<bool>
[src]
fn dyn_eq_in(
&self,
other: &dyn DynamicValue,
ctx: &mut dyn TermEqCtxMut
) -> Option<bool>
[src]Compare this term to another dynamic term
Provided methods
fn dyn_eq_term_in(
&self,
other: &Term,
ctx: &mut dyn TermEqCtxMut
) -> Option<bool>
[src]
fn dyn_eq_term_in(
&self,
other: &Term,
ctx: &mut dyn TermEqCtxMut
) -> Option<bool>
[src]Compare this term to another
fn dyn_eq_id_in(
&self,
other: &TermId,
ctx: &mut dyn TermEqCtxMut
) -> Option<bool>
[src]
fn dyn_eq_id_in(
&self,
other: &TermId,
ctx: &mut dyn TermEqCtxMut
) -> Option<bool>
[src]Compare this term to a term ID